\begin{tabbing}
$\forall$\=$A$:Type, ${\it eq}$:EqDecider($A$), $B$, $C$, $D$, $E$, $F$, $G$:($A$$\rightarrow$Type), $f$:$a$:$A$ fp$\rightarrow$ $B$($a$), $g$:$a$:$A$ fp$\rightarrow$ $C$($a$),\+
\\[0ex]$h$:$a$:$A$ fp$\rightarrow$ $D$($a$).
\-\\[0ex]($\forall$$a$:$A$. $B$($a$) $\subseteq$r $E$($a$))
\\[0ex]$\Rightarrow$ ($\forall$$a$:$A$. $C$($a$) $\subseteq$r $F$($a$))
\\[0ex]$\Rightarrow$ ($\forall$$a$:$A$. $D$($a$) $\subseteq$r $E$($a$))
\\[0ex]$\Rightarrow$ ($\forall$$a$:$A$. $D$($a$) $\subseteq$r $F$($a$))
\\[0ex]$\Rightarrow$ ($\forall$$a$:$A$. $F$($a$) $\subseteq$r $G$($a$))
\\[0ex]$\Rightarrow$ ($\forall$$a$:$A$. $E$($a$) $\subseteq$r $G$($a$))
\\[0ex]$\Rightarrow$ \{$h$ $\parallel$ $f$ $\Rightarrow$ $h$ $\parallel$ $g$ $\Rightarrow$ $h$ $\parallel$ $f$ $\oplus$ $g$\}
\end{tabbing}